Inference at * 1 2 1 
Iof proof for Lemma less-fast-fib:



1. n : 
2. 0 < n
3. a, b:.
3. {m:| 
3. {k:.
3. {(a = fib(k))  ((k  0)  (b = 0))  ((0 < k)  (b = fib(k - 1)))  (m = fib((n - 1)+k))} 
4. a : 
5. b : 
6. b@0:.
6. {m:| 
6. {k:.
6. {(a+b = fib(k))
6. { ((k  0)  (b@0 = 0))
6. { ((0 < k)  (b@0 = fib(k - 1)))
6. { (m = fib((n - 1)+k))} 
  {m:| 
  {k:.
  {(a = fib(k))  ((k  0)  (b = 0))  ((0 < k)  (b = fib(k - 1)))  (m = fib(n+k))}  

latex

 by InstHyp [a] (-1) 

latex

 1: .....wf..... NILNIL

 1:   a  
 2: 

 2: 7. {m:| 
 2: 7. {k:.
 2: 7. {(a+b = fib(k))
 2: 7. { ((k  0)  (a = 0))
 2: 7. { ((0 < k)  (a = fib(k - 1)))
 2: 7. { (m = fib((n - 1)+k))} 
 2:   {m:| 
 2:   {k:.
 2:   {(a = fib(k))  ((k  0)  (b = 0))  ((0 < k)  (b = fib(k - 1)))  (m = fib(n+k))} 
 .

Definitions

x:A. B(x)